The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas

摘要

Recent universal-hashing based approaches to sampling and counting cruciallydepend on the runtime performance of SAT solvers on formulas expressed as theconjunction of both CNF constraints and variable-width XOR constraints (knownas CNF-XOR formulas). In this paper, we present the first study of the runtimebehavior of SAT solvers equipped with XOR-reasoning techniques on randomCNF-XOR formulas. We empirically demonstrate that a state-of-the-art SAT solverscales exponentially on random CNF-XOR formulas across a wide range ofXOR-clause densities, peaking around the empirical phase-transition location.On the theoretical front, we prove that the solution space of a random CNF-XORformula 'shatters' at all nonzero XOR-clause densities into well-separatedcomponents, similar to the behavior seen in random CNF formulas known to bedifficult for many SAT algorithms.